1. Technical Field
The present application relates generally to an improved data processing system and method. More specifically, the present application is directed to a system and method for sequential equivalence checking for asynchronous verification.
2. Description of Related Art
Asynchronous verification is the process of verifying that integrated circuit designs with asynchronous crossings work correctly, i.e. that the logic will not behave inconsistently due to differences in timing conditions between two communicating clock regions. Verification of integrated circuit designs with asynchronous crossings is typically done by employing additional logic in simulation models of the integrated circuit design to thereby model the asynchronous crossing. User defined assertions/properties are then added to verify that the design conforms to its specification. Traditionally, this verification is done using simulation based techniques (user-defined as well as random test cases). However, it is difficult to model and verify the designs in simulation since the development of a test bench that exercises every possible combination of signals is a daunting task. Formal and semi-formal techniques can be used, which have the power to expose even the most probabilistically uncommon scenario that may result in a functional design failure, and ultimately have the power to prove that the design is correct, i.e. that no failing scenario exists. Developing a formal test bench for asynchronous verification is a time-consuming process without which formal techniques cannot directly provide benefit to such problems.
Much progress has been made in this area with the development of techniques/tools which try to automatically add assertions by analyzing the design. However, such techniques/tools are still incomplete, and often require specific design styles to work whatsoever. It is very difficult to assess whether the added assertions are complete, i.e. if there is a risk of a missed bug even if all the added assertions are proven correct. Presently, this is done through manual inspection by designers/verification engineers who will try to ensure that all needed assertions/properties have been added. Furthermore, the process of constraining input stimuli to avoid failures of the properties is an almost entirely manual process. The reliance on manual procedures greatly increases the amount of time to perform the verification process as well as increases the possibility of errors since human beings are prone to err.